\documentclass{article}
\usepackage[a4paper,margin=2cm,top=2.0cm,bottom=2.34cm]{geometry}
\usepackage[spanish,activeacute]{babel}
\usepackage{algo2symb}
\usepackage{tad}
\usepackage[T1]{fontenc}

\parskip=1.5ex
\pagestyle{empty}

\begin{document}

	\begin{tad}{IterSecu($\alpha$)}
		\generos{iterSecu($\alpha$)}
		\observadores
			\func{VerSecuSuby}{iterSecu($\alpha$)}{secu($\alpha$)}{}
			\func{VerSecu}{iterSecu($\alpha$)}{secu($\alpha$)}{}
		\generadores
			\func{CrearIt}{Secu($\alpha$)/s,Secu($\alpha$)/i}{iterSecu($\alpha$)}{esSufijo(s,i)}
		\otrasops
			\func{Eliminar}{iterSecu($\alpha$)}{iterSecu($\alpha$)}{$\neg$ Vacia?(i)}
		\axiomas
			\axioma{VerSecuSuby(CrearIt(s,i))}{i}
			\axioma{VerSecu(CrearIt(s,i))}{s}
			\axioma{Eliminar(CrearIt(s,i))}{CrearIt(take(s,long(s)-long(i))\&\& Fin(i),Fin(i))}
	\end{tad}

	\begin{tad}{Pendientes}
		\generos{pendientes}
		\observadores
			\func{Cola}{pendientes}{secu(vivienda)}{}
			\func{Catalogo}{pendientes}{catalogo}{}
		\generadores
			\func{Vacia}{catalogo}{pendientes}{}
			\func{Encolar}{pendientes, vivienda}{pendientes}{}
		\otrasops
			\func{ViviendasPorMaterial}{pendientes/p,material/m}{secu(vivienda)}{m $\in$ TodosLosMateriales(Catalogo(p))}
			\func{BorrarIesimoPorMaterial}{nat/i,material/m,pendientes/p}{pendientes}{i$<$long(ViviendasPorMaterial(p,m))}
		\axiomas
			\axioma{Cola(Vacia(c))}{$<>$}
			\axioma{Cola(Encolar(p, v))}{Cola(p) $\circ$ v}
			\axioma{Catalogo(Vacia(c))}{c}
			\axioma{Catalogo(Encolar(p,v))}{Catalogo(p)}
			\axioma{ViviendasPorMaterial(Vacia(c),m)}{$<>$}
			\axioma{ViviendasPorMaterial(Encolar(p,v),m)}{$\lif$ m $\in$ materiales(v) $\lthen$ ViviendasPorMaterial(p,m) $\circ$ v $\lelse$ ViviendasPorMaterial(p,m)}
			\axioma{BorrarIesimoPorMaterial(i,m,Encolar(p,v))}{\lif i=long(ViviendasPorMaterial(p,m)) \lthen p \lelse Encolar(BorrarIesimoPorMaterial(i,m,p),v)}
	\end{tad}
	
%	\begin{tad}{IterPendientes}
%		\generos{iterPendientes}
%		\observadores
%			\func{VerSecuSuby}{iterPendientes}{secu(vivienda)}{}
%			\func{VerPendientes}{iterPendientes}{pendientes}{}
%		\generadores
%			\func{CrearIterPendientes}{pendiente/p,secu(vivienda)/s,material/m}{iterPendientes}{esSufijo(s,ViviendasPorMaterial(p,m)) $\wedge$ m $\in$ TodosLosMateriales(Catalogo(c))}
%		\otrasops
%			\func{Eliminar}{iterPendientes/itp}{iterPendientes}{$\neg$ vacia(VerSecuSuby(itp))}
%		\axiomas
%			\axioma{VerSecuSuby(CrearIterPendientes(p,s,m))}{s}
%			\axioma{VerPendientes(CrearIterPendientes(p,s,m))}{p}
%			\axioma{Eliminar(CrearIterPendientes(p,s,m))}{CrearIterPendientes(BorrarIesimoPorMaterial(long(\\ViviendasPorMaterial(p,m))-long(s),m,p),Fin(s),m)}
%	\end{tad}

	\begin{tad}{IterPendientes}
		\generos{iterPendientes}
		\observadores
			\func{VerSecuSuby}{iterPendientes}{secu(vivienda)}{}
			\func{VerFiltrados}{iterPendientes}{secu(vivienda)}{}
		\generadores
			\func{CrearIterPendientes}{pendiente/p,secu(vivienda)/s,material/m}{iterPendientes}{m $\in$ TodosLosMateriales(Catalogo(p)) $\wedge_L$ esSufijo(s,ViviendasPorMaterial(p,m))}
		\otrasops
			\func{Eliminar}{iterPendientes/itp}{iterPendientes}{$\neg$ vacia(VerSecuSuby(itp))}
		\axiomas
			\axioma{VerSecuSuby(CrearIterPendientes(p,s,m))}{s}
			\axioma{VerFiltrados(CrearIterPendientes(p,s,m))}{ViviendasPorMaterial(p,m)}
			\axioma{Eliminar(CrearIterPendientes(p,s,m))}{CrearIterPendientes(BorrarIesimoPorMaterial(long(\\ViviendasPorMaterial(p,m))-long(s),m,p),Fin(s),m)}
	\end{tad}

	\begin{tad}{IterMateriales}
		\generos{iterMateriales}
		\observadores
			\func{VerConjSuby}{iterMateriales}{Conj(material)}{}
		\generadores
			\func{CrearIterMateriales}{multiconj\textunderscore materiales}{iterMateriales}{}
		\axiomas
			\axioma{VerConjSuby(CrearIterMateriales(ms))}{Conjunto(ms)}
	\end{tad}

	\begin{tad}{ARREGLO\_REDIMENSIONABLE($\alpha$)}

		\extiende{arreglo\_dimensionable($\alpha$)}
		\exporta{extender}

		\otrasops
			\func{extender}{ad($\alpha$)}{ad($\alpha$)}{}
			\func{copiarArreglo}{ad($\alpha$),ad($\alpha$),nat}{ad($\alpha$)}{tam(b) $\geq$ tam(a)}

		\axiomas
			\axioma{extender(a)}{copiarArreglo(a,crearArreglo(tam(a)+1),0)}\\
			\axioma{copiarArreglo(a,b,n)}{\lif n $<$ tam(a)\\ \hspace*{1em} \lthen \lif definido?(a,n) \\ \hspace*{4em} \lthen copiarArreglo(a\;,b[n]\; $\leftarrow$ \;a[n]\;,n+1)\\ \hspace*{4em} \lelse  copiarArreglo(a\;,b\;,n+1)\\ \hspace*{3.5em} \lfi \\ \hspace*{1em} \lelse b\\ \lfi}

\end{tad}

\end{document}
